i:Id, L:Knd List, x:Id, T:Type.
@i: only members of L affect x :T  Dsys
& (D:Dsys.
& (@i: only members of L affect x :T  D  D realizes es. @i only events in L change   x : T) 

latex

Definitions	t  T, x:A. B(x), es is an event system of D, ES, Type, {x:A| B(x) }, x:AB(x), @i only events in L change   x : T, Prop, x.A(x), {T}, P  Q, x. t(x), Dsys, D1  D2, D realizes es. P(es), A & B, Id, , MsgA, a = b, if b t else f fi, @i: A, Knd, type List, @i: only L affects x : t, only members of L affect x :t
Lemmas	frame-rule, Knd wf, ifthenelse wf, eq id wf, msga wf, ma-single-frame wf, ma-empty wf, Id wf, dsys wf, realizes-monotone-wrt-sub, frame-p wf, event system wf, d-es wf